M:MsgA.
{1of(M)  a:Id fp Type & 1of(2of(M))  k:Knd fp Type
{& 1of(2of(2of(M)))  x:Id fp 1of(M)(x)?Void
{& 1of(2of(2of(2of(M))))  a:Id fp State(1of(M))1of(2of(M))(locl(a))?TopProp
{& 1of(2of(2of(2of(2of(M)))))
{&  kx:KndId fp State(1of(M))Valtype(1of(2of(M));1of(kx))1of(M)(2of(kx))?Void
{& 1of(2of(2of(2of(2of(2of(M))))))
{&  kl:KndIdLnk fp
{&  (tg:Id
{&  ((State(1of(M))Valtype(1of(2of(M));1of(kl))(1of(2of(M))(rcv(2of(kl),tg))?Void List))) List
{& 1of(2of(2of(2of(2of(2of(2of(M)))))))  x:Id fp Knd List
{& 1of(2of(2of(2of(2of(2of(2of(2of(M))))))))  ltg:IdLnkId fp Knd List} 

latex

Definitions	t  T, P & Q, {T}, Valtype(da;k), MsgA, x:A. B(x)
Lemmas	msga wf